Nuprl Lemma : last-cons
11,40
postcript
pdf
x
:top,
as
:(top List). sqequal(last(cons(
x
;
as
)); if null(
as
) then
x
else last(
as
) fi )
latex
Definitions
hd(
l
)
,
i
<z
j
,
i
z
j
,
l
[
i
]
,
last(
L
)
,
top
,
t
T
,
x
:
A
.
B
(
x
)
,
ge(
i
;
j
)
,
P
Q
,
False
,
A
,
A
B
,
P
Q
,
lelt(
i
;
j
;
k
)
,
int_seg(
i
;
j
)
,
||
as
||
Lemmas
select
cons
tl
sq
,
length
cons
,
non
neg
length
,
length
wf1
,
top
wf
origin
x:top, as:(top List). sqequal(last(cons(x; as)); if null(as) then x else last(as) fi ) x:top, as:(top List). sqequal(last(cons(x; as)); if null(as) then x else last(as) fi ) 
z j
Tx:A. B(x)
Q
A B
Q